package sketch.specs;

public class SymbolicCommand {
	
	public static String[] jpfSymbolicOptions(String[] methodSignatures,  String driverClass) {
//		+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
//		+vm.classpath=.
//		+vm.storage.class=
//		+symbolic.method=remove(sym)
//		+search.multiple_errors=true
//		+jpf.report.console.finished=
//		TreeMapTest_testRemove
		String[] options = new String[7];
		
		options[0] = "+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory";
		options[1] = "+vm.classpath=.";
		options[2] = "+vm.storage.class=";
		options[3] = "+symbolic.method=";
		for(int i = 0; i < methodSignatures.length; i++) {
			if(i>0) {
				options[3] = options[3] + ",";
			}
			options[3] = options[3] + methodSignatures[i];
		}
		options[4] = "+search.multiple_errors=true";
		options[5] = "+jpf.report.console.finished=";
		options[6] = driverClass;
		
		return options;
	}
	
	public static String jpfSymbolicOptionsAsFlatString(String[] methodSignatures, String driverClass) {
		String[] strs = jpfSymbolicOptions(methodSignatures, driverClass);
		StringBuilder sb = new StringBuilder();
		
		int count = 0;
		for(String str : strs) {
			if(count > 0) {
				sb.append(",");
			}
			sb.append(str);
			count++;
		}
		
		return sb.toString();
	}
}